H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.081 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule FiniteMap

((eltsFM_GE :: FiniteMap Bool a -> Bool -> [a]) :: FiniteMap Bool a -> Bool -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

eltsFM_GE :: Ord b => FiniteMap b a -> b -> [a]

eltsFM_GE

fm fr

foldFM_GE (\key elt rest ->elt : rest) [] fr fm

foldFM_GE :: Ord a => (a -> c -> b -> b) -> b -> a -> FiniteMap a c -> b

foldFM_GE

k z fr EmptyFM

foldFM_GE

k z fr (Branch key elt _ fm_l fm_r)

key >= fr

foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

otherwise

foldFM_GE k z fr fm_r

module Maybe where

import qualified FiniteMap
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\keyeltrest→elt : rest

is transformed to

eltsFM_GE0 key elt rest = elt : rest

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule FiniteMap

((eltsFM_GE :: FiniteMap Bool a -> Bool -> [a]) :: FiniteMap Bool a -> Bool -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

eltsFM_GE :: Ord b => FiniteMap b a -> b -> [a]

eltsFM_GE

fm fr

foldFM_GE eltsFM_GE0 [] fr fm

eltsFM_GE0

key elt rest

elt : rest

foldFM_GE :: Ord c => (c -> a -> b -> b) -> b -> c -> FiniteMap c a -> b

foldFM_GE

k z fr EmptyFM

foldFM_GE

k z fr (Branch key elt _ fm_l fm_r)

key >= fr

foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

otherwise

foldFM_GE k z fr fm_r

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule FiniteMap

((eltsFM_GE :: FiniteMap Bool a -> Bool -> [a]) :: FiniteMap Bool a -> Bool -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

eltsFM_GE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_GE

fm fr

foldFM_GE eltsFM_GE0 [] fr fm

eltsFM_GE0

key elt rest

elt : rest

foldFM_GE :: Ord b => (b -> c -> a -> a) -> a -> b -> FiniteMap b c -> a

foldFM_GE

k z fr EmptyFM

foldFM_GE

k z fr (Branch key elt vw fm_l fm_r)

key >= fr

foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

otherwise

foldFM_GE k z fr fm_r

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

foldFM_GE k z fr EmptyFM = z

foldFM_GE k z fr (Branch key elt vw fm_l fm_r)

| key >= fr

= foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

| otherwise

= foldFM_GE k z fr fm_r

is transformed to

foldFM_GE k z fr EmptyFM = foldFM_GE3 k z fr EmptyFM

foldFM_GE k z fr (Branch key elt vw fm_l fm_r) = foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE1 k z fr key elt vw fm_l fm_r True = foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

foldFM_GE1 k z fr key elt vw fm_l fm_r False = foldFM_GE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_GE0 k z fr key elt vw fm_l fm_r True = foldFM_GE k z fr fm_r

foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r) = foldFM_GE1 k z fr key elt vw fm_l fm_r (key >= fr)

foldFM_GE3 k z fr EmptyFM = z

foldFM_GE3 wv ww wx wy = foldFM_GE2 wv ww wx wy

The following Function with conditions

compare x y

| x == y

= EQ

| x <= y

= LT

| otherwise

= GT

is transformed to

compare x y = compare3 x y

compare0 x y True = GT

compare2 x y True = EQ

compare2 x y False = compare1 x y (x <= y)

compare1 x y True = LT

compare1 x y False = compare0 x y otherwise

compare3 x y = compare2 x y (x == y)

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule FiniteMap

(eltsFM_GE :: FiniteMap Bool a -> Bool -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

eltsFM_GE :: Ord b => FiniteMap b a -> b -> [a]

eltsFM_GE

fm fr

foldFM_GE eltsFM_GE0 [] fr fm

eltsFM_GE0

key elt rest

elt : rest

foldFM_GE :: Ord a => (a -> b -> c -> c) -> c -> a -> FiniteMap a b -> c

foldFM_GE	k z fr EmptyFM	=	foldFM_GE3 k z fr EmptyFM
foldFM_GE	k z fr (Branch key elt vw fm_l fm_r)	=	foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE0

k z fr key elt vw fm_l fm_r True

foldFM_GE k z fr fm_r

foldFM_GE1	k z fr key elt vw fm_l fm_r True	=	foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l
foldFM_GE1	k z fr key elt vw fm_l fm_r False	=	foldFM_GE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_GE2

k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE1 k z fr key elt vw fm_l fm_r (key >= fr)

foldFM_GE3	k z fr EmptyFM	=	z
foldFM_GE3	wv ww wx wy	=	foldFM_GE2 wv ww wx wy

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="eltsFM_GE",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="eltsFM_GE wz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="eltsFM_GE wz3 wz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="foldFM_GE eltsFM_GE0 [] wz4 wz3",fontsize=16,color="burlywood",shape="triangle"];170[label="wz3/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];5 -> 170[label="",style="solid", color="burlywood", weight=9];
170 -> 6[label="",style="solid", color="burlywood", weight=3];
171[label="wz3/Branch wz30 wz31 wz32 wz33 wz34",fontsize=10,color="white",style="solid",shape="box"];5 -> 171[label="",style="solid", color="burlywood", weight=9];
171 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="foldFM_GE eltsFM_GE0 [] wz4 EmptyFM",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="foldFM_GE eltsFM_GE0 [] wz4 (Branch wz30 wz31 wz32 wz33 wz34)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="foldFM_GE3 eltsFM_GE0 [] wz4 EmptyFM",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="foldFM_GE2 eltsFM_GE0 [] wz4 (Branch wz30 wz31 wz32 wz33 wz34)",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="[]",fontsize=16,color="green",shape="box"];11[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (wz30 >= wz4)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (compare wz30 wz4 /= LT)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (compare wz30 wz4 == LT))",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (compare3 wz30 wz4 == LT))",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (compare2 wz30 wz4 (wz30 == wz4) == LT))",fontsize=16,color="burlywood",shape="box"];172[label="wz30/False",fontsize=10,color="white",style="solid",shape="box"];15 -> 172[label="",style="solid", color="burlywood", weight=9];
172 -> 16[label="",style="solid", color="burlywood", weight=3];
173[label="wz30/True",fontsize=10,color="white",style="solid",shape="box"];15 -> 173[label="",style="solid", color="burlywood", weight=9];
173 -> 17[label="",style="solid", color="burlywood", weight=3];
16[label="foldFM_GE1 eltsFM_GE0 [] wz4 False wz31 wz32 wz33 wz34 (not (compare2 False wz4 (False == wz4) == LT))",fontsize=16,color="burlywood",shape="box"];174[label="wz4/False",fontsize=10,color="white",style="solid",shape="box"];16 -> 174[label="",style="solid", color="burlywood", weight=9];
174 -> 18[label="",style="solid", color="burlywood", weight=3];
175[label="wz4/True",fontsize=10,color="white",style="solid",shape="box"];16 -> 175[label="",style="solid", color="burlywood", weight=9];
175 -> 19[label="",style="solid", color="burlywood", weight=3];
17[label="foldFM_GE1 eltsFM_GE0 [] wz4 True wz31 wz32 wz33 wz34 (not (compare2 True wz4 (True == wz4) == LT))",fontsize=16,color="burlywood",shape="box"];176[label="wz4/False",fontsize=10,color="white",style="solid",shape="box"];17 -> 176[label="",style="solid", color="burlywood", weight=9];
176 -> 20[label="",style="solid", color="burlywood", weight=3];
177[label="wz4/True",fontsize=10,color="white",style="solid",shape="box"];17 -> 177[label="",style="solid", color="burlywood", weight=9];
177 -> 21[label="",style="solid", color="burlywood", weight=3];
18[label="foldFM_GE1 eltsFM_GE0 [] False False wz31 wz32 wz33 wz34 (not (compare2 False False (False == False) == LT))",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 (not (compare2 False True (False == True) == LT))",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (compare2 True False (True == False) == LT))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="foldFM_GE1 eltsFM_GE0 [] True True wz31 wz32 wz33 wz34 (not (compare2 True True (True == True) == LT))",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="foldFM_GE1 eltsFM_GE0 [] False False wz31 wz32 wz33 wz34 (not (compare2 False False True == LT))",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 (not (compare2 False True False == LT))",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (compare2 True False False == LT))",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25[label="foldFM_GE1 eltsFM_GE0 [] True True wz31 wz32 wz33 wz34 (not (compare2 True True True == LT))",fontsize=16,color="black",shape="box"];25 -> 29[label="",style="solid", color="black", weight=3];
26[label="foldFM_GE1 eltsFM_GE0 [] False False wz31 wz32 wz33 wz34 (not (EQ == LT))",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 (not (compare1 False True (False <= True) == LT))",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (compare1 True False (True <= False) == LT))",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
29[label="foldFM_GE1 eltsFM_GE0 [] True True wz31 wz32 wz33 wz34 (not (EQ == LT))",fontsize=16,color="black",shape="box"];29 -> 33[label="",style="solid", color="black", weight=3];
30[label="foldFM_GE1 eltsFM_GE0 [] False False wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 (not (compare1 False True True == LT))",fontsize=16,color="black",shape="box"];31 -> 35[label="",style="solid", color="black", weight=3];
32[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (compare1 True False False == LT))",fontsize=16,color="black",shape="box"];32 -> 36[label="",style="solid", color="black", weight=3];
33[label="foldFM_GE1 eltsFM_GE0 [] True True wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];33 -> 37[label="",style="solid", color="black", weight=3];
34[label="foldFM_GE1 eltsFM_GE0 [] False False wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];34 -> 38[label="",style="solid", color="black", weight=3];
35[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 (not (LT == LT))",fontsize=16,color="black",shape="box"];35 -> 39[label="",style="solid", color="black", weight=3];
36[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (compare0 True False otherwise == LT))",fontsize=16,color="black",shape="box"];36 -> 40[label="",style="solid", color="black", weight=3];
37[label="foldFM_GE1 eltsFM_GE0 [] True True wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];37 -> 41[label="",style="solid", color="black", weight=3];
38 -> 83[label="",style="dashed", color="red", weight=0];
38[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 False wz31 (foldFM_GE eltsFM_GE0 [] False wz34)) False wz33",fontsize=16,color="magenta"];38 -> 84[label="",style="dashed", color="magenta", weight=3];
39[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 (not True)",fontsize=16,color="black",shape="box"];39 -> 44[label="",style="solid", color="black", weight=3];
40[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (compare0 True False True == LT))",fontsize=16,color="black",shape="box"];40 -> 45[label="",style="solid", color="black", weight=3];
41 -> 46[label="",style="dashed", color="red", weight=0];
41[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz31 (foldFM_GE eltsFM_GE0 [] True wz34)) True wz33",fontsize=16,color="magenta"];41 -> 47[label="",style="dashed", color="magenta", weight=3];
84 -> 92[label="",style="dashed", color="red", weight=0];
84[label="eltsFM_GE0 False wz31 (foldFM_GE eltsFM_GE0 [] False wz34)",fontsize=16,color="magenta"];84 -> 93[label="",style="dashed", color="magenta", weight=3];
83[label="foldFM_GE eltsFM_GE0 wz10 False wz33",fontsize=16,color="burlywood",shape="triangle"];181[label="wz33/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];83 -> 181[label="",style="solid", color="burlywood", weight=9];
181 -> 94[label="",style="solid", color="burlywood", weight=3];
182[label="wz33/Branch wz330 wz331 wz332 wz333 wz334",fontsize=10,color="white",style="solid",shape="box"];83 -> 182[label="",style="solid", color="burlywood", weight=9];
182 -> 95[label="",style="solid", color="burlywood", weight=3];
44[label="foldFM_GE1 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 False",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not (GT == LT))",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
47 -> 5[label="",style="dashed", color="red", weight=0];
47[label="foldFM_GE eltsFM_GE0 [] True wz34",fontsize=16,color="magenta"];47 -> 54[label="",style="dashed", color="magenta", weight=3];
47 -> 55[label="",style="dashed", color="magenta", weight=3];
46[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz31 wz6) True wz33",fontsize=16,color="burlywood",shape="triangle"];184[label="wz33/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];46 -> 184[label="",style="solid", color="burlywood", weight=9];
184 -> 56[label="",style="solid", color="burlywood", weight=3];
185[label="wz33/Branch wz330 wz331 wz332 wz333 wz334",fontsize=10,color="white",style="solid",shape="box"];46 -> 185[label="",style="solid", color="burlywood", weight=9];
185 -> 57[label="",style="solid", color="burlywood", weight=3];
93 -> 83[label="",style="dashed", color="red", weight=0];
93[label="foldFM_GE eltsFM_GE0 [] False wz34",fontsize=16,color="magenta"];93 -> 96[label="",style="dashed", color="magenta", weight=3];
93 -> 97[label="",style="dashed", color="magenta", weight=3];
92[label="eltsFM_GE0 False wz31 wz11",fontsize=16,color="black",shape="triangle"];92 -> 98[label="",style="solid", color="black", weight=3];
94[label="foldFM_GE eltsFM_GE0 wz10 False EmptyFM",fontsize=16,color="black",shape="box"];94 -> 101[label="",style="solid", color="black", weight=3];
95[label="foldFM_GE eltsFM_GE0 wz10 False (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];95 -> 102[label="",style="solid", color="black", weight=3];
52[label="foldFM_GE0 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 otherwise",fontsize=16,color="black",shape="box"];52 -> 60[label="",style="solid", color="black", weight=3];
53[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];53 -> 61[label="",style="solid", color="black", weight=3];
54[label="wz34",fontsize=16,color="green",shape="box"];55[label="True",fontsize=16,color="green",shape="box"];56[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz31 wz6) True EmptyFM",fontsize=16,color="black",shape="box"];56 -> 62[label="",style="solid", color="black", weight=3];
57[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz31 wz6) True (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];57 -> 63[label="",style="solid", color="black", weight=3];
96[label="wz34",fontsize=16,color="green",shape="box"];97[label="[]",fontsize=16,color="green",shape="box"];98[label="wz31 : wz11",fontsize=16,color="green",shape="box"];101[label="foldFM_GE3 eltsFM_GE0 wz10 False EmptyFM",fontsize=16,color="black",shape="box"];101 -> 106[label="",style="solid", color="black", weight=3];
102[label="foldFM_GE2 eltsFM_GE0 wz10 False (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];102 -> 107[label="",style="solid", color="black", weight=3];
60[label="foldFM_GE0 eltsFM_GE0 [] True False wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];60 -> 66[label="",style="solid", color="black", weight=3];
61[label="foldFM_GE1 eltsFM_GE0 [] False True wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];61 -> 67[label="",style="solid", color="black", weight=3];
62[label="foldFM_GE3 eltsFM_GE0 (eltsFM_GE0 True wz31 wz6) True EmptyFM",fontsize=16,color="black",shape="box"];62 -> 68[label="",style="solid", color="black", weight=3];
63[label="foldFM_GE2 eltsFM_GE0 (eltsFM_GE0 True wz31 wz6) True (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];63 -> 69[label="",style="solid", color="black", weight=3];
106[label="wz10",fontsize=16,color="green",shape="box"];107[label="foldFM_GE1 eltsFM_GE0 wz10 False wz330 wz331 wz332 wz333 wz334 (wz330 >= False)",fontsize=16,color="black",shape="box"];107 -> 109[label="",style="solid", color="black", weight=3];
66 -> 5[label="",style="dashed", color="red", weight=0];
66[label="foldFM_GE eltsFM_GE0 [] True wz34",fontsize=16,color="magenta"];66 -> 73[label="",style="dashed", color="magenta", weight=3];
66 -> 74[label="",style="dashed", color="magenta", weight=3];
67 -> 83[label="",style="dashed", color="red", weight=0];
67[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz31 (foldFM_GE eltsFM_GE0 [] False wz34)) False wz33",fontsize=16,color="magenta"];67 -> 88[label="",style="dashed", color="magenta", weight=3];
68[label="eltsFM_GE0 True wz31 wz6",fontsize=16,color="black",shape="triangle"];68 -> 77[label="",style="solid", color="black", weight=3];
69 -> 78[label="",style="dashed", color="red", weight=0];
69[label="foldFM_GE1 eltsFM_GE0 (eltsFM_GE0 True wz31 wz6) True wz330 wz331 wz332 wz333 wz334 (wz330 >= True)",fontsize=16,color="magenta"];69 -> 79[label="",style="dashed", color="magenta", weight=3];
109[label="foldFM_GE1 eltsFM_GE0 wz10 False wz330 wz331 wz332 wz333 wz334 (compare wz330 False /= LT)",fontsize=16,color="black",shape="box"];109 -> 111[label="",style="solid", color="black", weight=3];
73[label="wz34",fontsize=16,color="green",shape="box"];74[label="True",fontsize=16,color="green",shape="box"];88 -> 68[label="",style="dashed", color="red", weight=0];
88[label="eltsFM_GE0 True wz31 (foldFM_GE eltsFM_GE0 [] False wz34)",fontsize=16,color="magenta"];88 -> 99[label="",style="dashed", color="magenta", weight=3];
77[label="wz31 : wz6",fontsize=16,color="green",shape="box"];79 -> 68[label="",style="dashed", color="red", weight=0];
79[label="eltsFM_GE0 True wz31 wz6",fontsize=16,color="magenta"];78[label="foldFM_GE1 eltsFM_GE0 wz9 True wz330 wz331 wz332 wz333 wz334 (wz330 >= True)",fontsize=16,color="black",shape="triangle"];78 -> 100[label="",style="solid", color="black", weight=3];
111[label="foldFM_GE1 eltsFM_GE0 wz10 False wz330 wz331 wz332 wz333 wz334 (not (compare wz330 False == LT))",fontsize=16,color="black",shape="box"];111 -> 114[label="",style="solid", color="black", weight=3];
99 -> 83[label="",style="dashed", color="red", weight=0];
99[label="foldFM_GE eltsFM_GE0 [] False wz34",fontsize=16,color="magenta"];99 -> 103[label="",style="dashed", color="magenta", weight=3];
99 -> 104[label="",style="dashed", color="magenta", weight=3];
100[label="foldFM_GE1 eltsFM_GE0 wz9 True wz330 wz331 wz332 wz333 wz334 (compare wz330 True /= LT)",fontsize=16,color="black",shape="box"];100 -> 105[label="",style="solid", color="black", weight=3];
114[label="foldFM_GE1 eltsFM_GE0 wz10 False wz330 wz331 wz332 wz333 wz334 (not (compare3 wz330 False == LT))",fontsize=16,color="black",shape="box"];114 -> 117[label="",style="solid", color="black", weight=3];
103[label="wz34",fontsize=16,color="green",shape="box"];104[label="[]",fontsize=16,color="green",shape="box"];105[label="foldFM_GE1 eltsFM_GE0 wz9 True wz330 wz331 wz332 wz333 wz334 (not (compare wz330 True == LT))",fontsize=16,color="black",shape="box"];105 -> 108[label="",style="solid", color="black", weight=3];
117[label="foldFM_GE1 eltsFM_GE0 wz10 False wz330 wz331 wz332 wz333 wz334 (not (compare2 wz330 False (wz330 == False) == LT))",fontsize=16,color="burlywood",shape="box"];193[label="wz330/False",fontsize=10,color="white",style="solid",shape="box"];117 -> 193[label="",style="solid", color="burlywood", weight=9];
193 -> 120[label="",style="solid", color="burlywood", weight=3];
194[label="wz330/True",fontsize=10,color="white",style="solid",shape="box"];117 -> 194[label="",style="solid", color="burlywood", weight=9];
194 -> 121[label="",style="solid", color="burlywood", weight=3];
108[label="foldFM_GE1 eltsFM_GE0 wz9 True wz330 wz331 wz332 wz333 wz334 (not (compare3 wz330 True == LT))",fontsize=16,color="black",shape="box"];108 -> 110[label="",style="solid", color="black", weight=3];
120[label="foldFM_GE1 eltsFM_GE0 wz10 False False wz331 wz332 wz333 wz334 (not (compare2 False False (False == False) == LT))",fontsize=16,color="black",shape="box"];120 -> 124[label="",style="solid", color="black", weight=3];
121[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (compare2 True False (True == False) == LT))",fontsize=16,color="black",shape="box"];121 -> 125[label="",style="solid", color="black", weight=3];
110[label="foldFM_GE1 eltsFM_GE0 wz9 True wz330 wz331 wz332 wz333 wz334 (not (compare2 wz330 True (wz330 == True) == LT))",fontsize=16,color="burlywood",shape="box"];195[label="wz330/False",fontsize=10,color="white",style="solid",shape="box"];110 -> 195[label="",style="solid", color="burlywood", weight=9];
195 -> 112[label="",style="solid", color="burlywood", weight=3];
196[label="wz330/True",fontsize=10,color="white",style="solid",shape="box"];110 -> 196[label="",style="solid", color="burlywood", weight=9];
196 -> 113[label="",style="solid", color="burlywood", weight=3];
124[label="foldFM_GE1 eltsFM_GE0 wz10 False False wz331 wz332 wz333 wz334 (not (compare2 False False True == LT))",fontsize=16,color="black",shape="box"];124 -> 128[label="",style="solid", color="black", weight=3];
125[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (compare2 True False False == LT))",fontsize=16,color="black",shape="box"];125 -> 129[label="",style="solid", color="black", weight=3];
112[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 (not (compare2 False True (False == True) == LT))",fontsize=16,color="black",shape="box"];112 -> 115[label="",style="solid", color="black", weight=3];
113[label="foldFM_GE1 eltsFM_GE0 wz9 True True wz331 wz332 wz333 wz334 (not (compare2 True True (True == True) == LT))",fontsize=16,color="black",shape="box"];113 -> 116[label="",style="solid", color="black", weight=3];
128[label="foldFM_GE1 eltsFM_GE0 wz10 False False wz331 wz332 wz333 wz334 (not (EQ == LT))",fontsize=16,color="black",shape="box"];128 -> 132[label="",style="solid", color="black", weight=3];
129[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (compare1 True False (True <= False) == LT))",fontsize=16,color="black",shape="box"];129 -> 133[label="",style="solid", color="black", weight=3];
115[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 (not (compare2 False True False == LT))",fontsize=16,color="black",shape="box"];115 -> 118[label="",style="solid", color="black", weight=3];
116[label="foldFM_GE1 eltsFM_GE0 wz9 True True wz331 wz332 wz333 wz334 (not (compare2 True True True == LT))",fontsize=16,color="black",shape="box"];116 -> 119[label="",style="solid", color="black", weight=3];
132[label="foldFM_GE1 eltsFM_GE0 wz10 False False wz331 wz332 wz333 wz334 (not False)",fontsize=16,color="black",shape="box"];132 -> 138[label="",style="solid", color="black", weight=3];
133[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (compare1 True False False == LT))",fontsize=16,color="black",shape="box"];133 -> 139[label="",style="solid", color="black", weight=3];
118[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 (not (compare1 False True (False <= True) == LT))",fontsize=16,color="black",shape="box"];118 -> 122[label="",style="solid", color="black", weight=3];
119[label="foldFM_GE1 eltsFM_GE0 wz9 True True wz331 wz332 wz333 wz334 (not (EQ == LT))",fontsize=16,color="black",shape="box"];119 -> 123[label="",style="solid", color="black", weight=3];
138[label="foldFM_GE1 eltsFM_GE0 wz10 False False wz331 wz332 wz333 wz334 True",fontsize=16,color="black",shape="box"];138 -> 143[label="",style="solid", color="black", weight=3];
139[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (compare0 True False otherwise == LT))",fontsize=16,color="black",shape="box"];139 -> 144[label="",style="solid", color="black", weight=3];
122[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 (not (compare1 False True True == LT))",fontsize=16,color="black",shape="box"];122 -> 126[label="",style="solid", color="black", weight=3];
123[label="foldFM_GE1 eltsFM_GE0 wz9 True True wz331 wz332 wz333 wz334 (not False)",fontsize=16,color="black",shape="box"];123 -> 127[label="",style="solid", color="black", weight=3];
143 -> 83[label="",style="dashed", color="red", weight=0];
143[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 False wz331 (foldFM_GE eltsFM_GE0 wz10 False wz334)) False wz333",fontsize=16,color="magenta"];143 -> 148[label="",style="dashed", color="magenta", weight=3];
143 -> 149[label="",style="dashed", color="magenta", weight=3];
144[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (compare0 True False True == LT))",fontsize=16,color="black",shape="box"];144 -> 150[label="",style="solid", color="black", weight=3];
126[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 (not (LT == LT))",fontsize=16,color="black",shape="box"];126 -> 130[label="",style="solid", color="black", weight=3];
127[label="foldFM_GE1 eltsFM_GE0 wz9 True True wz331 wz332 wz333 wz334 True",fontsize=16,color="black",shape="box"];127 -> 131[label="",style="solid", color="black", weight=3];
148[label="wz333",fontsize=16,color="green",shape="box"];149 -> 92[label="",style="dashed", color="red", weight=0];
149[label="eltsFM_GE0 False wz331 (foldFM_GE eltsFM_GE0 wz10 False wz334)",fontsize=16,color="magenta"];149 -> 154[label="",style="dashed", color="magenta", weight=3];
149 -> 155[label="",style="dashed", color="magenta", weight=3];
150[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not (GT == LT))",fontsize=16,color="black",shape="box"];150 -> 156[label="",style="solid", color="black", weight=3];
130[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 (not True)",fontsize=16,color="black",shape="box"];130 -> 134[label="",style="solid", color="black", weight=3];
131 -> 46[label="",style="dashed", color="red", weight=0];
131[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz331 (foldFM_GE eltsFM_GE0 wz9 True wz334)) True wz333",fontsize=16,color="magenta"];131 -> 135[label="",style="dashed", color="magenta", weight=3];
131 -> 136[label="",style="dashed", color="magenta", weight=3];
131 -> 137[label="",style="dashed", color="magenta", weight=3];
154[label="wz331",fontsize=16,color="green",shape="box"];155 -> 83[label="",style="dashed", color="red", weight=0];
155[label="foldFM_GE eltsFM_GE0 wz10 False wz334",fontsize=16,color="magenta"];155 -> 162[label="",style="dashed", color="magenta", weight=3];
156[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 (not False)",fontsize=16,color="black",shape="box"];156 -> 163[label="",style="solid", color="black", weight=3];
134[label="foldFM_GE1 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 False",fontsize=16,color="black",shape="box"];134 -> 140[label="",style="solid", color="black", weight=3];
135[label="wz331",fontsize=16,color="green",shape="box"];136[label="wz333",fontsize=16,color="green",shape="box"];137[label="foldFM_GE eltsFM_GE0 wz9 True wz334",fontsize=16,color="burlywood",shape="triangle"];201[label="wz334/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];137 -> 201[label="",style="solid", color="burlywood", weight=9];
201 -> 141[label="",style="solid", color="burlywood", weight=3];
202[label="wz334/Branch wz3340 wz3341 wz3342 wz3343 wz3344",fontsize=10,color="white",style="solid",shape="box"];137 -> 202[label="",style="solid", color="burlywood", weight=9];
202 -> 142[label="",style="solid", color="burlywood", weight=3];
162[label="wz334",fontsize=16,color="green",shape="box"];163[label="foldFM_GE1 eltsFM_GE0 wz10 False True wz331 wz332 wz333 wz334 True",fontsize=16,color="black",shape="box"];163 -> 164[label="",style="solid", color="black", weight=3];
140[label="foldFM_GE0 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 otherwise",fontsize=16,color="black",shape="box"];140 -> 145[label="",style="solid", color="black", weight=3];
141[label="foldFM_GE eltsFM_GE0 wz9 True EmptyFM",fontsize=16,color="black",shape="box"];141 -> 146[label="",style="solid", color="black", weight=3];
142[label="foldFM_GE eltsFM_GE0 wz9 True (Branch wz3340 wz3341 wz3342 wz3343 wz3344)",fontsize=16,color="black",shape="box"];142 -> 147[label="",style="solid", color="black", weight=3];
164 -> 83[label="",style="dashed", color="red", weight=0];
164[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 True wz331 (foldFM_GE eltsFM_GE0 wz10 False wz334)) False wz333",fontsize=16,color="magenta"];164 -> 165[label="",style="dashed", color="magenta", weight=3];
164 -> 166[label="",style="dashed", color="magenta", weight=3];
145[label="foldFM_GE0 eltsFM_GE0 wz9 True False wz331 wz332 wz333 wz334 True",fontsize=16,color="black",shape="box"];145 -> 151[label="",style="solid", color="black", weight=3];
146[label="foldFM_GE3 eltsFM_GE0 wz9 True EmptyFM",fontsize=16,color="black",shape="box"];146 -> 152[label="",style="solid", color="black", weight=3];
147[label="foldFM_GE2 eltsFM_GE0 wz9 True (Branch wz3340 wz3341 wz3342 wz3343 wz3344)",fontsize=16,color="black",shape="box"];147 -> 153[label="",style="solid", color="black", weight=3];
165[label="wz333",fontsize=16,color="green",shape="box"];166 -> 68[label="",style="dashed", color="red", weight=0];
166[label="eltsFM_GE0 True wz331 (foldFM_GE eltsFM_GE0 wz10 False wz334)",fontsize=16,color="magenta"];166 -> 167[label="",style="dashed", color="magenta", weight=3];
166 -> 168[label="",style="dashed", color="magenta", weight=3];
151 -> 137[label="",style="dashed", color="red", weight=0];
151[label="foldFM_GE eltsFM_GE0 wz9 True wz334",fontsize=16,color="magenta"];152[label="wz9",fontsize=16,color="green",shape="box"];153 -> 78[label="",style="dashed", color="red", weight=0];
153[label="foldFM_GE1 eltsFM_GE0 wz9 True wz3340 wz3341 wz3342 wz3343 wz3344 (wz3340 >= True)",fontsize=16,color="magenta"];153 -> 157[label="",style="dashed", color="magenta", weight=3];
153 -> 158[label="",style="dashed", color="magenta", weight=3];
153 -> 159[label="",style="dashed", color="magenta", weight=3];
153 -> 160[label="",style="dashed", color="magenta", weight=3];
153 -> 161[label="",style="dashed", color="magenta", weight=3];
167[label="wz331",fontsize=16,color="green",shape="box"];168 -> 83[label="",style="dashed", color="red", weight=0];
168[label="foldFM_GE eltsFM_GE0 wz10 False wz334",fontsize=16,color="magenta"];168 -> 169[label="",style="dashed", color="magenta", weight=3];
157[label="wz3344",fontsize=16,color="green",shape="box"];158[label="wz3340",fontsize=16,color="green",shape="box"];159[label="wz3342",fontsize=16,color="green",shape="box"];160[label="wz3343",fontsize=16,color="green",shape="box"];161[label="wz3341",fontsize=16,color="green",shape="box"];169[label="wz334",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_GE(wz9, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
new_foldFM_GE1(wz9, True, wz331, wz332, wz333, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
new_foldFM_GE1(wz9, True, wz331, wz332, wz333, wz334, h) → new_foldFM_GE0(wz331, new_foldFM_GE2(wz9, wz334, h), wz333, h)
new_foldFM_GE0(wz31, wz6, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE1(new_eltsFM_GE0(wz31, wz6, h), wz330, wz331, wz332, wz333, wz334, h)
new_foldFM_GE1(wz9, False, wz331, wz332, wz333, wz334, h) → new_foldFM_GE(wz9, wz334, h)

The TRS R consists of the following rules:

new_eltsFM_GE0(wz31, wz6, h) → :(wz31, wz6)
new_foldFM_GE3(wz31, wz6, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE10(new_eltsFM_GE0(wz31, wz6, h), wz330, wz331, wz332, wz333, wz334, h)
new_foldFM_GE2(wz9, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE10(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
new_foldFM_GE10(wz9, False, wz331, wz332, wz333, wz334, h) → new_foldFM_GE2(wz9, wz334, h)
new_foldFM_GE10(wz9, True, wz331, wz332, wz333, wz334, h) → new_foldFM_GE3(wz331, new_foldFM_GE2(wz9, wz334, h), wz333, h)
new_foldFM_GE3(wz31, wz6, EmptyFM, h) → new_eltsFM_GE0(wz31, wz6, h)
new_foldFM_GE2(wz9, EmptyFM, h) → wz9

The set Q consists of the following terms:

new_foldFM_GE2(x0, EmptyFM, x1)
new_foldFM_GE3(x0, x1, EmptyFM, x2)
new_eltsFM_GE0(x0, x1, x2)
new_foldFM_GE10(x0, False, x1, x2, x3, x4, x5)
new_foldFM_GE2(x0, Branch(x1, x2, x3, x4, x5), x6)
new_foldFM_GE10(x0, True, x1, x2, x3, x4, x5)
new_foldFM_GE3(x0, x1, Branch(x2, x3, x4, x5, x6), x7)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_GE1(wz9, False, wz331, wz332, wz333, wz334, h) → new_foldFM_GE(wz9, wz334, h)
The graph contains the following edges 1 >= 1, 6 >= 2, 7 >= 3
new_foldFM_GE1(wz9, True, wz331, wz332, wz333, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
The graph contains the following edges 1 >= 1, 6 > 2, 6 > 3, 6 > 4, 6 > 5, 6 > 6, 7 >= 7
new_foldFM_GE1(wz9, True, wz331, wz332, wz333, wz334, h) → new_foldFM_GE0(wz331, new_foldFM_GE2(wz9, wz334, h), wz333, h)
The graph contains the following edges 3 >= 1, 5 >= 3, 7 >= 4
new_foldFM_GE0(wz31, wz6, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE1(new_eltsFM_GE0(wz31, wz6, h), wz330, wz331, wz332, wz333, wz334, h)
The graph contains the following edges 3 > 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7
new_foldFM_GE(wz9, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4, 2 > 5, 2 > 6, 3 >= 7

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_GE4(wz10, Branch(False, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(wz10, wz334, h)
new_foldFM_GE4(wz10, Branch(True, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(new_eltsFM_GE0(wz331, new_foldFM_GE5(wz10, wz334, h), h), wz333, h)
new_foldFM_GE4(wz10, Branch(False, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(new_eltsFM_GE00(wz331, new_foldFM_GE5(wz10, wz334, h), h), wz333, h)
new_foldFM_GE4(wz10, Branch(True, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(wz10, wz334, h)

The TRS R consists of the following rules:

new_eltsFM_GE0(wz31, wz6, h) → :(wz31, wz6)
new_foldFM_GE5(wz10, Branch(False, wz331, wz332, wz333, wz334), h) → new_foldFM_GE5(new_eltsFM_GE00(wz331, new_foldFM_GE5(wz10, wz334, h), h), wz333, h)
new_foldFM_GE5(wz10, Branch(True, wz331, wz332, wz333, wz334), h) → new_foldFM_GE5(new_eltsFM_GE0(wz331, new_foldFM_GE5(wz10, wz334, h), h), wz333, h)
new_eltsFM_GE00(wz31, wz11, h) → :(wz31, wz11)
new_foldFM_GE5(wz10, EmptyFM, h) → wz10

The set Q consists of the following terms:

new_foldFM_GE5(x0, EmptyFM, x1)
new_eltsFM_GE0(x0, x1, x2)
new_eltsFM_GE00(x0, x1, x2)
new_foldFM_GE5(x0, Branch(False, x1, x2, x3, x4), x5)
new_foldFM_GE5(x0, Branch(True, x1, x2, x3, x4), x5)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_GE4(wz10, Branch(False, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(wz10, wz334, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
new_foldFM_GE4(wz10, Branch(True, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(new_eltsFM_GE0(wz331, new_foldFM_GE5(wz10, wz334, h), h), wz333, h)
The graph contains the following edges 2 > 2, 3 >= 3
new_foldFM_GE4(wz10, Branch(False, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(new_eltsFM_GE00(wz331, new_foldFM_GE5(wz10, wz334, h), h), wz333, h)
The graph contains the following edges 2 > 2, 3 >= 3
new_foldFM_GE4(wz10, Branch(True, wz331, wz332, wz333, wz334), h) → new_foldFM_GE4(wz10, wz334, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_GE6(True, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_GE6(True, wz34, h)
new_foldFM_GE6(True, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_GE6(True, wz34, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_GE6(True, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_GE6(True, wz34, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
new_foldFM_GE6(True, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_GE6(True, wz34, h)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 3 >= 3

foldFM_GE	k z fr EmptyFM	= foldFM_GE3 k z fr EmptyFM
foldFM_GE	k z fr (Branch key elt vw fm_l fm_r)	= foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE1	k z fr key elt vw fm_l fm_r True	= foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l
foldFM_GE1	k z fr key elt vw fm_l fm_r False	= foldFM_GE0 k z fr key elt vw fm_l fm_r otherwise

compare2	x y True	= EQ
compare2	x y False	= compare1 x y (x <= y)

compare1	x y True	= LT
compare1	x y False	= compare0 x y otherwise